Schreiber thesis Wellen

$\,$

This page collects material related to this thesis that I once advised:

---

• Felix Wellen,

  Formalizing Cartan Geometry in Modal Homotopy Type Theory

  PhD Thesis, KIT 2017

  
  

  thesis: pdf,

  archived version: web

  talk slides: pdf

  preprint version: arXiv:1806.05966,

  HoTT-Agda code: DCHoTT-Agda.

on basics of differential geometry (smooth manifolds and G-structures) generalized to higher Cartan geometry and formalized in modal homotopy type theory (modal homotopy type theory, cohesive homotopy type theory).

---

$\,$

This thesis implements a fragment of the axioms of differential cohesion (Schreiber 13) for synthetic differential geometry, formalized in homotopy type theory and implemented in the Agda proof management system:

A modal operator is introduced (see Schreiber 15 for exposition) which is interpreted as an “infinitesimal shape” modality $\Im$. For $X$ any homotopy type then the standard interpretation of the type $\Im X$ is the result of “identifying infinitesimally close points in $X$”.

(By synthetic PDE theory (Khavkine-Schreiber 17) the dependent types over $\Im X$ have the interpretation of being partial differential equations with free variables ranging in $X$. The linear dependent types over $\Im X$ are also known as D-modules, as used in geometric representation theory.)

Using this infinitesimal shape modality $\Im$ the thesis presents a formalization of the concept of manifold in the type theory. Via the homotopy theoretic interpretation of the type theory the interpretation of such “manifold types” is really as étale ∞-stacks $X$ (Schreiber 13).

The main theorem of the thesis shows that the infinitesimal disk bundle of any such manifold $X$ is a fiber ∞-bundle which is associated to a principal ∞-bundle (Nikolaus-Schreiber-Stevenson 12): its frame bundle.

This solves the first of the three problems in modal type theory that had been posed in

• Urs Schreiber, Some thoughts on the future of modal homotopy type theory, talk at Homotopy Type Theory and Univalent Foundations - Mini-Symposium, within the German Mathematical Society meeting 2015 21st - 25th Sept, Hamburg (talk notes pdf)

Classically, the concept of frame bundle is the foundation of all genuine geometry, via Cartan geometry: Equipping the frame bundle of a manifold $X$ with torsion-free G-structure means to equip $X$ with a flavor of geometry, depending on the choice of $G$, such as (pseudo-)Riemannian geometry, conformal geometry, complex geometry, symplectic geometry etc. pp. The moduli stacks of all given $G$-structures on a given manifold are of central interest in the classical theory, such as the moduli stacks of complex structures, or the moduli stacks of conformal structures.

In order to lift classical Cartan geometry from classical manifolds to higher Cartan geometry on étale ∞-stacks, the thesis closes by formalizing the concept of torsion-free G-structure on manifold types. Due to the homotopy-theoretic interpretation this is really a formalization of higher (∞-group) $G$-structures on étale ∞-stacks, including also examples such as string structures or Fivebrane structures.
Finally the thesis demonstrates the construction of the (higher) moduli stacks of such torsion-free G-structures

$\,$

For exposition see

• Felix Wellen, Geometry in Modal HoTT, talk at Geometry in Modal HoTT (2019) (video recording)

and tutorial 6 in:

• Dan Licata, Felix Wellen, Synthetic Mathematics in Modal Dependent Type Theories, tutorial at Types, Homotopy Theory and Verification (2018)

  Tutorial 1, Dan Licata: A Fibrational Framework for Modal Simple Type Theories (recording)

  Tutorial 2, Felix Wellen: The Shape Modality in Real cohesive HoTT and Covering Spaces (recording)

  Tutorial 3, Dan Licata: Discrete and Codiscrete Modalities in Cohesive HoTT (recording)

  Tutorial 4, Felix Wellen, Discrete and Codiscrete Modalities in Cohesive HoTT, II (recording)

  Tutorial 5, Dan Licata: A Fibrational Framework for Modal Dependent Type Theories (recording)

  Tutorial 6, Felix Wellen: Differential Cohesive HoTT, (recording)

  slides:

  Dan Licata, Synthetic Mathematics in Modal Dependent Type Theories, notes for tutorial at Types, Homotopy Theory and Verification, 2018 (pdf)

also

• Egbert Rijke, Modal descent, talk at Geometry in Modal HoTT (2019) (video recording)

$\,$

For more exposition see also at Formalizing Cartan Geometry in Modal HoTT and at geometry of physics – manifolds and orbifolds.

For more higher differential geometry-background see

• Urs Schreiber, Higher Cartan Geometry

For further development concerning jet bundles and PDEs, see

• Igor Khavkine, Urs Schreiber, Synthetic geometry of differential equations (arXiv:1701.06238, v2, talk slides, talk video)

$\,$

---

$\,$